Sections-9.agda:4,1-7
Could not parse the left-hand side ⟨ _ ⟩_
Operators used in the grammar:
  None
when scope checking the left-hand side ⟨ _ ⟩_ in the definition of
⟨_⟩_
